UnequalRelevance.agda:11,7-8
(A → A) !=< (.A → A) because one is a relevant function type and
the other is an irrelevant function type
when checking that the expression f has type .A → A
